/*
 * File:   main.c
 * Authors: 06-39550, 06-39538
 *
 * Created on 27 de enero de 2011, 07:37 PM
 */

#include <stdio.h>
#include <stdlib.h>
#include <limits.h>
#include <string.h>
#include <unistd.h>
#include <math.h>
#include <time.h>

#define MALLOC  "MALLOC MAIN: no hay suficiente memoria para continuar.\n"
#define USAGE   "USAGE: ./p1 <archivo_entrada>\n"
#define MAXLINE 26254
#define TRUE    (0==0)
#define FALSE   (!(0==0))
/**una instancia de grado 9 necesita a lo sumo cerca de 26250 chars*/

/** cierra el programa en caso de error */
void salir(char *msj) {
  printf("%s", msj);
  exit(EXIT_FAILURE);
}

/*Calcula la cantidad máxima de caracteres que va a ocupar la cantidad de
 clausulas*/
int magia(int num) {
  double aux2;
  aux2 = num * (num - 1) / 2;
  aux2 = num * num * (2 + 4 * aux2);
  return (int) aux2;
}

/*Genera las clausulas Tipo 1, "cada casilla debe contener al menos un numero*/
void generarClausulasT1(int tamInstancia, FILE *salida) {
  int nVariables = pow(tamInstancia, 3);
  int i;
  for (i = 1; i <= nVariables; i++) {
    fprintf(salida, "%d ", i);
    if (i % tamInstancia == 0)
      fprintf(salida, "0\n");
  }

}

/*Genera las clausulas Tipo 2, "una casilla no puede contener 2 numeros distintos*/
void generarClausulasT2(int tamInstancia, FILE *salida) {
  int i, j, d1, d2, aux1;
  int tam2 = tamInstancia * tamInstancia;
  for (i = 0; i < tamInstancia; i++) {
    for (j = 0; j < tamInstancia; j++) {
      for (d1 = 1; d1 < tamInstancia; d1++) {
        for (d2 = d1 + 1; d2 <= tamInstancia; d2++) {
          aux1 = (i * tam2) + (j * tamInstancia);
          fprintf(salida, "-%d -%d 0\n", aux1 + d1, aux1 + d2);
        }
      }
    }
  }

}

/*Genera las clausulas Tipo 3, no pueden haber numeros repetidos en la misma
 fila, columna o cuadrante*/
void generarClausulasT3(int tamInstancia, FILE *salida) {
  int count, d, i, j, aux, aux2, aux3, aux4, aux5, aux6;
  int tam = sqrt(tamInstancia);
  int tam2 = tamInstancia * tamInstancia;
  for (count = 0; count < tamInstancia; count++) {
    aux = (count * tam2);
    aux2 = (count * tamInstancia);
    aux3 = (count / tam) * tam2 * tam + (count % tam) * tamInstancia * tam;
    for (d = 1; d <= tamInstancia; d++) {
      aux4 = aux + d;
      aux5 = aux2 + d;
      aux6 = aux3 + d;
      for (i = 0; i < (tamInstancia - 1); i++) {
        for (j = i + 1; j < tamInstancia; j++) {
          fprintf(salida, "-%d -%d 0\n", aux4 + (i * tamInstancia), aux4 + (j * tamInstancia));
          fprintf(salida, "-%d -%d 0\n", aux5 + (i * tam2), aux5 + (j * tam2));
          fprintf(salida, "-%d -%d 0\n", aux6 + (i / tam) * tam2 + (i % tam) * tamInstancia, aux6 + (j / tam) * tam2 + (j % tam) * tamInstancia);
        }
      }
    }
  }
}

/*Verifica si la instancia de entrada es correcta, no tiene 2 numeros en el mismo
 cuadrante*/
int duplicadoCuadrado(int *linea, int casilla, int grado) {
  int tam = grado*grado;
  if (((int) (casilla / tam)) % grado == grado - 1)
    return -1;
  int j, i;
  i = casilla - casilla % grado;
  while (((int) (i / tam)) % grado != grado - 1) {
    i += tam;
    for (j = 0; j < grado; j++) {
      if (linea[casilla] == linea[i + j]) {
        return i + j;
      }
    }
  };
  return -1;
}

/*Verifica si la instancia de entrada es correcta, no tiene 2 numeros en la misma
 columna*/
int duplicadoVertical(int *linea, int casilla, int grado) {
  int tam = grado*grado;
  int i = casilla;
  while (i < pow(tam, 2)) {
    i += tam;
    if (linea[i] != 0 && linea[casilla] == linea[i]) {
      return i;
    }
  }
  return -1;
}

/*Verifica si la instancia de entrada es correcta, no tiene 2 numeros en la misma
 fila*/
int duplicadoHorizontal(int *linea, int casilla, int grado) {
  int tam = grado*grado;
  int i = 1;
  while (i < tam - casilla % ((int) tam)) {
    if (linea[casilla + i] != 0 && linea[casilla] == linea[casilla + i]) {
      return casilla + i;
    }
    i++;
  }
  return -1;
}

/*Grafica la salida del SAT solver como un tablero de SUDOKU*/
int toTex(int tamInst) {
  int nVariables, sol, i, j, tam2, aux1, tamLinea;
  char *aux;
  char *linea;
  FILE *sat, *salida;
  tamLinea = 1000000;
  linea = (char *) malloc(sizeof (char) * tamLinea);
  if (linea == NULL) {
    salir(MALLOC);
  }
  sat = fopen("SAT_RESULT.txt", "r");
  if (sat == NULL) {
    printf("No se encontró SAT_RESULT.txt.\n");
    exit(0);
  }

  salida = fopen("SUDOKU.txt", "a");
  fgets(linea, tamLinea, sat);
  while (linea != NULL && linea[0] != 's')
    fgets(linea, tamLinea, sat);
  aux = strtok(linea, " "); // "s"
  aux = strtok(NULL, " "); // "TYPE"
  aux = strtok(NULL, " "); // "SOLUTION"
  sol = atoi(aux);
  if (!sol) {
    printf("NADA QUE DIBUJAR\n");
    return (EXIT_SUCCESS);
  }
  fprintf(salida, "\n\nSe encontro la siguiente solución!\n\n");
  aux = strtok(NULL, " "); // "VARIABLES"
  nVariables = atoi(aux);
  tam2 = tamInst * tamInst;
  fgets(linea, tamLinea, sat);
  sol = strlen(linea);
  linea[sol - 1] = '\0';
  aux = strtok(linea, " ");
  i = 1;
  j = 0;
  while (aux != NULL) {
    aux1 = atoi(aux);
    aux = strtok(NULL, " ");
    if (aux1 < 0)
      continue;
    aux1 = aux1 % tam2;
    if (aux1 == 0)
      fprintf(salida, "%d ", tam2);
    else
      fprintf(salida, "%d ", aux1);
    if (i % tam2 == 0) {
      fprintf(salida, "\n");
      j++;
      i = 0;
    } else if (i % tamInst == 0)
      fprintf(salida, " | ");
    if (j / tamInst == 1) {
      fprintf(salida, "\n");
      j = 0;
    }
    i++;
  }

  fclose(salida);
  fclose(sat);
  free(linea);
}

/** version para problemas con tamInstancia > 3*/
void generarClausulasIni(char* linea, int tamInstancia, FILE *salida) {
  int aux1, i, aux2;
  int sum = 0;
  char *token;
  aux2 = magia(tamInstancia);
  fprintf(salida, "p cnf %d %d\n", tamInstancia*tamInstancia, aux2);
  token = strtok(linea, " ,");
  for (i = 0; i < tamInstancia * tamInstancia; i++) {
    if (token == NULL) {
      printf("SUDOKU incorrecto...\n");
      exit(EXIT_FAILURE);
    }
    aux1 = atoi(token);
    if (aux1 != 0) {
      fprintf(salida, "\n%d 0", i * tamInstancia + aux1);
      sum++;
    }
    token = strtok(NULL, " ,");
  }
  fprintf(salida, "\n");
  aux1 = tamInstancia * tamInstancia;
  aux2 = aux2 - aux1;
  aux1 = aux1 * tamInstancia;
  fseek(salida, 0, SEEK_SET);
  fprintf(salida, "p cnf %d %d", aux1, aux2 + sum);
  fseek(salida, 0, SEEK_END);
}

/** version para problemas con tamInstancia <= 3*/
void generarClausulasIni1(char* linea, int tamInstancia, FILE *salida) {
  int aux1, i, aux2;
  int sum = 0;
  aux2 = magia(tamInstancia);
  fprintf(salida, "p cnf %d %d\n", tamInstancia*tamInstancia, aux2);
  for (i = 0; i < tamInstancia * tamInstancia; i++) {
    aux1 = linea[i] - '0';
    if (aux1 != 0) {
      sum++;
      fprintf(salida, "\n%d 0", i * tamInstancia + aux1);
    }
  }
  fprintf(salida, "\n");
  aux1 = tamInstancia * tamInstancia;
  aux2 = aux2 - aux1;
  aux1 = aux1 * tamInstancia;
  fseek(salida, 0, SEEK_SET);
  fprintf(salida, "p cnf %d %d", aux1, aux2 + sum);
  fseek(salida, 0, SEEK_END);
}

/*Verifica si un SUDOKU es correcto*/
int verificarSudoku(int *linea, int grado) {
  // Esta variable se va moviendo casilla por casilla en el sudoku para
  // verificar que el sudoku sea valido.
  int casilla = 0;
  int tam = grado*grado;
  int dh, dv, dc;
  while (casilla < tam * tam) {
    if (linea[casilla] != 0) {
      dh = duplicadoHorizontal(linea, casilla, grado);
      dv = duplicadoVertical(linea, casilla, grado);
      dc = duplicadoCuadrado(linea, casilla, grado);
      if (dh != -1) {
        printf("Duplicado horizontal el numero %d en posiciones %d (%d,%d), %d (%d,%d)\n",
                linea[casilla],
                casilla, casilla / tam, casilla % tam,
                dh, dh / tam, dh % tam);
        return FALSE;
      }
      if (dv != -1) {
        printf("Duplicado vertical el numero %d en posiciones %d (%d,%d), %d (%d,%d)\n",
                linea[casilla],
                casilla, casilla / tam, casilla % tam,
                dv, dv / tam, dv % tam);
        return FALSE;
      }
      if (dc != -1) {
        //            printf("DC: %d , TAM: %d\n",dc,tam);
        printf("Duplicado en el cuadrado el numero %d en posiciones %d (%d,%d), %d (%d,%d)\n",
                linea[casilla],
                casilla, casilla / tam, casilla % tam,
                dc, dc / tam, dc % tam);
        return FALSE;
      }
    }
    casilla++;
  }
  return TRUE;
}

int* duplicarLinea(char* linea, int tam) {
  char *aux, *token;
  int i;
  int *ret = (int*) malloc(sizeof (int) *pow(tam, 4));
  if (ret == NULL)
    salir(MALLOC);
  aux = (char*) malloc(sizeof (MAXLINE));
  if (aux == NULL)
    salir(MALLOC);
  strcpy(aux, linea);
  token = strtok(aux, " ,");
  //printf("Instancia: ");
  for (i = 0; token != NULL; i++) {
    ret[i] = atoi(token);
    //  printf(" %d",ret[i]);
    token = strtok(NULL, " ,");
  }
  //printf("\n");
  return ret;
}

int* chartoint(char* linea, int tam) {
  char *aux = (char*) malloc(sizeof (char) *pow(tam, 4));
  if (aux == NULL)
    salir(MALLOC);
  int i;
  int *ret = (int*) malloc(sizeof (int) *pow(tam, 4));
  if (ret == NULL)
    salir(MALLOC);
  strcpy(aux, linea);
  //printf("Instancia: 3 %s.\n",aux);
  for (i = 0; i < pow(tam, 2); i++) {
    ret[i] = aux[i] - '0';
    //  printf(" %d",ret[i]);
  }
  //printf("\n");
  free(aux);
  return ret;
}

/*Genera todas las clausulas que representan una instancia de SUDOKU a partir
 del archivo de entrada*/
int generarClausulas(char* linea, FILE *salida) {
  char *borrar;
  int *lin;
  int grado, nCasillas, tam;
  int sudokuCorrecto = TRUE;
  /** libero espacio para leer los problemas*/
  if (linea == NULL) {
    salir(MALLOC);
  }
  borrar = linea;

  printf("Instancia: %s\n", linea);
  /*  Aqui, se puede saber el tamano de la linea, y el espacio en memoria necesario para guardar
      la linea, x lo que se podria calcular el espacio, guardarlo en el nuevo espacio y hacerle
      free a linea
   */
  /** obtenemos el tamaño del problema, suponemos grado <= 9 (81x81) */
  grado = linea[0] - '0'; /** mas rapido que atoi */
  tam = grado * grado; /** numeros diferentes en el sudoku */
  nCasillas = tam * tam; /** cantidad de casillas en el sudoku */
  linea = linea + 2; /** nos desplazamos al inicio del tablero */
  if (grado >= 4)
    lin = duplicarLinea(linea, tam);
  else
    lin = chartoint(linea, tam);
  sudokuCorrecto = verificarSudoku(lin, grado); /** verifico que el sudoku leido sea correcto */
  if (sudokuCorrecto) {
    /** genero las clausulas de los elementos en el tablero */
    if (grado > 3) {
      generarClausulasIni(linea, tam, salida);
    } else {
      generarClausulasIni1(linea, tam, salida);
    }
    /** genero las clausulas dependientes al grado del problema*/
    generarClausulasT1(tam, salida);
    generarClausulasT2(tam, salida);
    generarClausulasT3(tam, salida);
  } else {
    grado = 0;
  }
  free(borrar); /** liberamos MAXLINE bytes de memoria */
  free(lin);
  return grado;
}

/*Int ---> String*/
char* itoa(int value, char* result, int base) {
  // check that the base if valid
  if (base < 2 || base > 36) {
    *result = '\0';
    return result;
  }

  char* ptr = result, *ptr1 = result, tmp_char;
  int tmp_value;

  do {
    tmp_value = value;
    value /= base;
    *ptr++ = "zyxwvutsrqponmlkjihgfedcba9876543210123456789abcdefghijklmnopqrstuvwxyz" [35 + (tmp_value - value * base)];
  } while (value);

  // Apply negative sign
  if (tmp_value < 0) *ptr++ = '-';
  *ptr-- = '\0';
  while (ptr1 < ptr) {
    tmp_char = *ptr;
    *ptr-- = *ptr1;
    *ptr1++ = tmp_char;
  }
  return result;
}

int main(int argc, char** argv) {
  int i = 0, grado = TRUE, todo = FALSE;
  FILE *entrada;
  char* linea = (char*) malloc(LINE_MAX);
  if (linea == NULL)
    salir(MALLOC);
  char* iString;
  char cnf[] = "./CNF/";
  char sat_result[] = "./SAT_RESULT/";
  char soluciones[] = "./SOLUCIONES/";
  char txt[] = ".txt";
  char jose[] = "./jose ";
  if (argc < 2) {
    salir(USAGE);
  }
 /*Verifico si la opcion -a fue ingresada*/
  if (strcmp(argv[1], "-a") == 0) {
    todo = TRUE;
    entrada = fopen(argv[2], "r");
    if (entrada == NULL) {
      printf("No se encontró archivo de entrada\n");
      exit(0);
    }
  } else {
    entrada = fopen(argv[1], "r");
    if (entrada == NULL) {
      printf("No se encontró archivo de entrada\n");
      exit(0);
    }
  }

  /*Creo las carpetas donde se van a colocar las salidas*/
  system("mkdir CNF");
  system("mkdir SAT_RESULT");
  system("mkdir SOLUCIONES");
  /** guardo el problema equivalente en un archivo CNF.txt*/
  while (fgets(linea, MAXLINE, entrada)) {
    FILE *salida;
    char *cmd0 = (char*) malloc(100);
    if (cmd0 == NULL)
      salir(MALLOC);
    char *cmd = (char*) malloc(100);
    if (cmd == NULL)
      salir(MALLOC);
    iString = (char*) malloc(10);
    if (iString == NULL)
      salir(MALLOC);
    itoa(i, iString, 10);
    cmd0[0] = '\0';
    cmd[0] = '\0';
    strcat(cmd0, cnf);
    strcat(cmd0, "CNF");
    strcat(cmd0, iString);
    strcat(cmd0, txt);
    // printf("CNF: %s\n", cmd0);
    salida = fopen(cmd0, "w+");
    grado = generarClausulas(linea, salida);
    //      exit(0);
    fclose(salida);
    if (grado > 0) {
      strcat(cmd,"time -poSUDOKU.txt ");
      strcat(cmd, jose);
      strcat(cmd, cmd0);
      //CORRO JOSE
      system(cmd);
      cmd[0] = '\0';
      strcat(cmd, "./zchaff/zchaff ");
      strcat(cmd, cmd0);
      //CORRO ZCHAFF
      //  system(cmd);
      toTex(grado);
      system("more SUDOKU.txt");
      cmd0[0] = '\0';
      cmd[0] = '\0';
      strcat(cmd0, soluciones);
      strcat(cmd0, "SUDOKU");
      strcat(cmd0, iString);
      strcat(cmd0, txt);
      strcat(cmd, "mv SUDOKU.txt ");
      strcat(cmd, cmd0);
      //MUEVO SUDOKU.txt a su carpeta
      system(cmd);
      cmd0[0] = '\0';
      cmd[0] = '\0';
      strcat(cmd, sat_result);
      strcat(cmd, "SAT_RESULT");
      strcat(cmd, iString);
      strcat(cmd, txt);
      strcat(cmd0, "mv SAT_RESULT.txt ");
      strcat(cmd0, cmd);
      //MUEVO SAT_RESULT A SU CARPETA
      system(cmd0);
      free(cmd0);
      free(cmd);
      free(iString);
      i++;
    }
    if (!todo)
      break;
    linea = (char*) malloc(LINE_MAX);
    if (linea == NULL)
      salir(MALLOC);
  }

  return (EXIT_SUCCESS);
}
